/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.transform;

import java.util.Collections;
import java.util.Iterator;
import java.util.List;

import alloy.ast.ASTDepthFirstReplacer;
import alloy.ast.ASTDepthFirstVisitor;
import alloy.ast.Expr;
import alloy.ast.Exprs;
import alloy.ast.Formula;
import alloy.ast.Function;
import alloy.ast.InvocablePara;
import alloy.ast.InvocationExpr;
import alloy.ast.InvocationFormula;
import alloy.ast.Location;
import alloy.ast.Module;
import alloy.ast.ModuleInfo;
import alloy.ast.Node;
import alloy.ast.Predicate;
import alloy.semantic.ExprTypeCheckVisitor;
import alloy.semantic.LocalScope;
import alloy.semantic.TypeErrorReporter;
import alloy.util.AlloyConstants;
import alloy.util.Dbg;

/**
 * <p>Inlines invocations so that they are properly replaced by the body
 * of the invoked function.  There are two major cases for invocation inlining.
 * <ul>
 * <li>Invocation is a formula: In this case, the invocation is replaced
 * with a copy of the formula body of the predicate.  All appearances in the predicate body copy of
 * the predicate's formal arguments are replaced by the appropriate parameter from the invocation.
 * Note that if the predicate has been skolemized, its inlining is instead handled by
 * the methods of {@link FunctionSkolemizer}.
 * <li>Invocation is an expression: In this case, the invocation is replaced
 * with a copy of the expression body of the function.  All appearances in the function body copy of
 * the functions's formal arguments are replaced by the appropriate parameter from the invocation.
 * Note that if the function has been skolemized, its inlining is instead handled by
 * the methods of {@link FunctionSkolemizer}.
 *
 * <p>Note that whenever a formal is replaced by a parameter, the type information
 * associated with the parameter must be maintained.  Also, shadowing must be checked
 * so that formals which have been shadowed are not replaced in that scope.  Also,
 * type parameters for functions must be replaced by the actual types wherever they
 * appear in the body.
 */

public class InvocationInlineVisitor
    extends ASTDepthFirstReplacer
    implements AlloyConstants {

    /**
     * module scope of module where current invocation resides.  used
     * in typechecking if invoked function resides in another module.
     */
    private ModuleInfo _invModuleInfo;

    /**
       function skolemizer used to skolemize recursive functions
       in model
    */
    private FunctionSkolemizer _fs;

    public InvocationInlineVisitor(FunctionSkolemizer fs_) {
        _fs = fs_;
        
    }

   public InvocationInlineVisitor(FunctionSkolemizer fs, ModuleInfo modInfo) {
       this(fs);
       _invModuleInfo = modInfo;
   }
    /**
     * inlines invocations found in bodies of invocables.  this method should
     * be called before an instance of InvocationInlineVisitor is applied to
     * the specification as a whole.
     * @param invocable_ list of invocables, sorted such that no invocable contains
     * an invocation of a invocable appearing after it in the list.
     * @see ConstructInvocationGraphVisitor
     */
    public static void inlineFunctionBodyInvocations(List invocables_,
                                                     FunctionSkolemizer fs_) {
        InvocationInlineVisitor visitor = new InvocationInlineVisitor(fs_);
        Iterator invocableIter = invocables_.iterator();
        while (invocableIter.hasNext()) {
            InvocablePara invocable = (InvocablePara) invocableIter.next();
            // set visitor's module scope properly
            visitor._invModuleInfo =
                ((Module)invocable.getParent().getParent()).getModuleInfo();
            invocable.applyReturnVisitor(visitor);
        }
    }

    public Object visit(Module module_) {
        // set the module scope
        _invModuleInfo =
        module_.getModuleInfo();
        visit((Node) module_);
        return module_;
    }

    /**
     * Inline an invocation used as a formula.
     */
    public Object visit(InvocationFormula invocationFormula_) {
        // first, apply visitor to parameters
        // Dbg.info("visiting " + invocationFormula_.nodeString());
        Formula ret = invocationFormula_;
        // Dbg.info("inlining args");
        invocationFormula_.setReceiver((Expr) invocationFormula_.getReceiver().applyReturnVisitor(this));
        invocationFormula_.setExprs((Exprs) invocationFormula_.getExprs().applyReturnVisitor(this));

        // now, handle current invocation - get invoked predicate
        Predicate invokedPredicate = (Predicate)invocationFormula_.getInvocable();
        // check if invocation is to skolemized function
        if (_fs.isSkolemized(invokedPredicate)) {
            Formula f = _fs.inlineSkolemized(invocationFormula_);
            invocationFormula_.nodeString();
            f.annotateReplacing("inlining of recursive function invocation " +
                                invocationFormula_.nodeString(),
                                invocationFormula_);
            return f;
        }

        //Dbg.info(invocationFormula_.replacednodeString());
        // make copy of body
        Formula inlineCopy = (Formula) invokedPredicate.getFormula().copy();
        // replace formals by parameters in body, and replace var types by
        // instantiated types
        inlineCopy =
            (Formula) inlineCopy.applyReturnVisitor(
                new ExprAndTypeReplaceVisitor(invokedPredicate,
                                              invocationFormula_));

	
	//System.out.println("========================");
	//System.out.println("Inlining " + invocationFormula_);
	// typecheck the inlined copy so that all the expressions within the formula
	// have the most specific type that can be deduced from the actual parameters
        try {
	inlineCopy = (Formula) ExprTypeCheckVisitor.typecheckNode((Node)inlineCopy.copy(),
								  _invModuleInfo, new LocalScope(), 
								  Collections.EMPTY_MAP, 
								  new TypeErrorReporter(false));
	
        } catch (ExprTypeCheckVisitor.TypeCheckException tce ) {
            // do nothing -- all typechecking errors at this point
            // are false alarms
        }
        
    //System.out.println("***********************");
    //System.out.println(inlineCopy.nodeString() + " copied");
    //System.out.println("copy location " + inlineCopy.getLocation());
    //System.out.println("copy invocation locations " + inlineCopy.getInvocationLocations());
    //System.out.println("***********************");
        // Dbg.info("inlining result: " + inlineCopy.nodeString());
        // replace invocation by modified function body
        inlineCopy.annotateReplacing(
            "inlining of function invocation " + invocationFormula_.nodeString(),
            invocationFormula_);
    inlineCopy.applyVisitor(
            new AddInvocationLocationVisitor(invocationFormula_.getLocation()));
    // inline invocations in resulting formula
        return inlineCopy.applyReturnVisitor(this);
    }

    /**
     * Inline an invocation used as an expression.
     */
    public Object visit(InvocationExpr invocationExpr_) {
        // Dbg.info("visiting " + invocationExpr_.nodeString());
        // Dbg.info("inlining args");
        invocationExpr_.setReceiver((Expr) invocationExpr_.getReceiver().applyReturnVisitor(this));
        invocationExpr_.setExprs((Exprs) invocationExpr_.getExprs().applyReturnVisitor(this));

        // now handle current invocation
        // get invoked function
        Function invokedFunction = (Function)invocationExpr_.getInvocable();
        // if skolemized function is invoked, don't use trick
        //if (_fs.isSkolemized(invokedFunction)) return null;
        Dbg.chk(invokedFunction != null, "invocation " + invocationExpr_.nodeString() + " at "
                + invocationExpr_.getLocation().toString() + " has null invokedFunction");

        Expr inlineCopy = (Expr) invokedFunction.getExpression().copy();
        // do replacement on expression
        inlineCopy =
            (Expr) inlineCopy.applyReturnVisitor(
                new ExprAndTypeReplaceVisitor(invokedFunction,
                                              invocationExpr_));

	
	// typecheck the inlined copy so that all the expressions within the formula
	// have the most specific type that can be deduced from the actual parameters
		//System.out.println("========================");
			try {
	inlineCopy = (Expr) ExprTypeCheckVisitor.typecheckNode((Node)inlineCopy.copy(),
							       _invModuleInfo, 
							       new LocalScope(), 
							       Collections.EMPTY_MAP,
							       new TypeErrorReporter(false));
	
	        } catch (ExprTypeCheckVisitor.TypeCheckException tce ) {
	            // do nothing -- all typechecking errors at this point
	            // are false alarms
	        }
	
	    //System.out.println("Inlining " + invocationExpr_ + " : " + inlineCopy.getType());
		//System.out.println("========================");
	

        // Dbg.info("inlining result: " + inlineCopy.nodeString());
        // replace invocation with expression
        inlineCopy.annotateReplacing("inlining of invocation " + invocationExpr_.nodeString(),
                                     invocationExpr_);
        inlineCopy.applyVisitor(new AddInvocationLocationVisitor(invocationExpr_.getLocation()));
        // inline invocations in resulting formula
        return (Expr) inlineCopy.applyReturnVisitor(this);
    }

    private static class AddInvocationLocationVisitor extends ASTDepthFirstVisitor {
        private final Location _invocationLocation;

        AddInvocationLocationVisitor(Location invocationLocation_) { _invocationLocation = invocationLocation_; }

        public void visit(Node n_) {
            super.visit(n_);
            n_.addInvocationLocation(_invocationLocation);
        }
    }
}
